'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, h(mark(X)) -> mark(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(ok(X)) -> ok(h(X))
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))
, active^#(c(X)) -> c_1(d^#(X))
, active^#(h(X)) -> c_2(c^#(d(X)))
, active^#(f(X)) -> c_3(f^#(active(X)))
, active^#(h(X)) -> c_4(h^#(active(X)))
, f^#(mark(X)) -> c_5(f^#(X))
, h^#(mark(X)) -> c_6(h^#(X))
, proper^#(f(X)) -> c_7(f^#(proper(X)))
, proper^#(c(X)) -> c_8(c^#(proper(X)))
, proper^#(g(X)) -> c_9(g^#(proper(X)))
, proper^#(d(X)) -> c_10(d^#(proper(X)))
, proper^#(h(X)) -> c_11(h^#(proper(X)))
, f^#(ok(X)) -> c_12(f^#(X))
, c^#(ok(X)) -> c_13(c^#(X))
, g^#(ok(X)) -> c_14(g^#(X))
, d^#(ok(X)) -> c_15(d^#(X))
, h^#(ok(X)) -> c_16(h^#(X))
, top^#(mark(X)) -> c_17(top^#(proper(X)))
, top^#(ok(X)) -> c_18(top^#(active(X)))}
The usable rules are:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
The estimated dependency graph contains the following edges:
{active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
==> {c^#(ok(X)) -> c_13(c^#(X))}
{active^#(c(X)) -> c_1(d^#(X))}
==> {d^#(ok(X)) -> c_15(d^#(X))}
{active^#(h(X)) -> c_2(c^#(d(X)))}
==> {c^#(ok(X)) -> c_13(c^#(X))}
{active^#(f(X)) -> c_3(f^#(active(X)))}
==> {f^#(ok(X)) -> c_12(f^#(X))}
{active^#(f(X)) -> c_3(f^#(active(X)))}
==> {f^#(mark(X)) -> c_5(f^#(X))}
{active^#(h(X)) -> c_4(h^#(active(X)))}
==> {h^#(ok(X)) -> c_16(h^#(X))}
{active^#(h(X)) -> c_4(h^#(active(X)))}
==> {h^#(mark(X)) -> c_6(h^#(X))}
{f^#(mark(X)) -> c_5(f^#(X))}
==> {f^#(ok(X)) -> c_12(f^#(X))}
{f^#(mark(X)) -> c_5(f^#(X))}
==> {f^#(mark(X)) -> c_5(f^#(X))}
{h^#(mark(X)) -> c_6(h^#(X))}
==> {h^#(ok(X)) -> c_16(h^#(X))}
{h^#(mark(X)) -> c_6(h^#(X))}
==> {h^#(mark(X)) -> c_6(h^#(X))}
{proper^#(f(X)) -> c_7(f^#(proper(X)))}
==> {f^#(ok(X)) -> c_12(f^#(X))}
{proper^#(f(X)) -> c_7(f^#(proper(X)))}
==> {f^#(mark(X)) -> c_5(f^#(X))}
{proper^#(c(X)) -> c_8(c^#(proper(X)))}
==> {c^#(ok(X)) -> c_13(c^#(X))}
{proper^#(g(X)) -> c_9(g^#(proper(X)))}
==> {g^#(ok(X)) -> c_14(g^#(X))}
{proper^#(d(X)) -> c_10(d^#(proper(X)))}
==> {d^#(ok(X)) -> c_15(d^#(X))}
{proper^#(h(X)) -> c_11(h^#(proper(X)))}
==> {h^#(ok(X)) -> c_16(h^#(X))}
{proper^#(h(X)) -> c_11(h^#(proper(X)))}
==> {h^#(mark(X)) -> c_6(h^#(X))}
{f^#(ok(X)) -> c_12(f^#(X))}
==> {f^#(ok(X)) -> c_12(f^#(X))}
{f^#(ok(X)) -> c_12(f^#(X))}
==> {f^#(mark(X)) -> c_5(f^#(X))}
{c^#(ok(X)) -> c_13(c^#(X))}
==> {c^#(ok(X)) -> c_13(c^#(X))}
{g^#(ok(X)) -> c_14(g^#(X))}
==> {g^#(ok(X)) -> c_14(g^#(X))}
{d^#(ok(X)) -> c_15(d^#(X))}
==> {d^#(ok(X)) -> c_15(d^#(X))}
{h^#(ok(X)) -> c_16(h^#(X))}
==> {h^#(ok(X)) -> c_16(h^#(X))}
{h^#(ok(X)) -> c_16(h^#(X))}
==> {h^#(mark(X)) -> c_6(h^#(X))}
{top^#(mark(X)) -> c_17(top^#(proper(X)))}
==> {top^#(ok(X)) -> c_18(top^#(active(X)))}
{top^#(mark(X)) -> c_17(top^#(proper(X)))}
==> {top^#(mark(X)) -> c_17(top^#(proper(X)))}
{top^#(ok(X)) -> c_18(top^#(active(X)))}
==> {top^#(ok(X)) -> c_18(top^#(active(X)))}
{top^#(ok(X)) -> c_18(top^#(active(X)))}
==> {top^#(mark(X)) -> c_17(top^#(proper(X)))}
We consider the following path(s):
1) { active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(ok(X)) -> c_12(f^#(X))
, f^#(mark(X)) -> c_5(f^#(X))}
The usable rules for this path are the following:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(ok(X)) -> c_12(f^#(X))
, f^#(mark(X)) -> c_5(f^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{f^#(mark(X)) -> c_5(f^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(mark(X)) -> c_5(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(f(X)) -> c_3(f^#(active(X)))}
and weakly orienting the rules
{f^#(mark(X)) -> c_5(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(ok(X)) -> c_12(f^#(X))}
and weakly orienting the rules
{ active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(mark(X)) -> c_5(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(ok(X)) -> c_12(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [13]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [9]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [2]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(h(X)) -> mark(c(d(X)))}
and weakly orienting the rules
{ f^#(ok(X)) -> c_12(f^#(X))
, active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(mark(X)) -> c_5(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(h(X)) -> mark(c(d(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [8]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))}
and weakly orienting the rules
{ active(h(X)) -> mark(c(d(X)))
, f^#(ok(X)) -> c_12(f^#(X))
, active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(mark(X)) -> c_5(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, f^#(ok(X)) -> c_12(f^#(X))
, active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(mark(X)) -> c_5(f^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, f^#(ok(X)) -> c_12(f^#(X))
, active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(mark(X)) -> c_5(f^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(9) -> 11
, f^#_0(3) -> 18
, f^#_0(9) -> 18
, c_5_0(18) -> 18
, c_12_0(18) -> 18}
2) { active^#(h(X)) -> c_4(h^#(active(X)))
, h^#(ok(X)) -> c_16(h^#(X))
, h^#(mark(X)) -> c_6(h^#(X))}
The usable rules for this path are the following:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, active^#(h(X)) -> c_4(h^#(active(X)))
, h^#(ok(X)) -> c_16(h^#(X))
, h^#(mark(X)) -> c_6(h^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{h^#(mark(X)) -> c_6(h^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{h^#(mark(X)) -> c_6(h^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
h^#(x1) = [1] x1 + [3]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(h(X)) -> c_4(h^#(active(X)))}
and weakly orienting the rules
{h^#(mark(X)) -> c_6(h^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(h(X)) -> c_4(h^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [5]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
h^#(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{h^#(ok(X)) -> c_16(h^#(X))}
and weakly orienting the rules
{ active^#(h(X)) -> c_4(h^#(active(X)))
, h^#(mark(X)) -> c_6(h^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{h^#(ok(X)) -> c_16(h^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [2]
h^#(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(h(X)) -> mark(c(d(X)))}
and weakly orienting the rules
{ h^#(ok(X)) -> c_16(h^#(X))
, active^#(h(X)) -> c_4(h^#(active(X)))
, h^#(mark(X)) -> c_6(h^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(h(X)) -> mark(c(d(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [8]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
h^#(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))}
and weakly orienting the rules
{ active(h(X)) -> mark(c(d(X)))
, h^#(ok(X)) -> c_16(h^#(X))
, active^#(h(X)) -> c_4(h^#(active(X)))
, h^#(mark(X)) -> c_6(h^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
h^#(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, h^#(ok(X)) -> c_16(h^#(X))
, active^#(h(X)) -> c_4(h^#(active(X)))
, h^#(mark(X)) -> c_6(h^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, h^#(ok(X)) -> c_16(h^#(X))
, active^#(h(X)) -> c_4(h^#(active(X)))
, h^#(mark(X)) -> c_6(h^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(2) -> 2
, ok_0(2) -> 2
, active^#_0(2) -> 1
, h^#_0(2) -> 1
, c_6_0(1) -> 1
, c_16_0(1) -> 1}
3) { top^#(mark(X)) -> c_17(top^#(proper(X)))
, top^#(ok(X)) -> c_18(top^#(active(X)))}
The usable rules for this path are the following:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, top^#(mark(X)) -> c_17(top^#(proper(X)))
, top^#(ok(X)) -> c_18(top^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{top^#(ok(X)) -> c_18(top^#(active(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{top^#(ok(X)) -> c_18(top^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [14]
c_17(x1) = [1] x1 + [0]
c_18(x1) = [1] x1 + [2]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))}
and weakly orienting the rules
{top^#(ok(X)) -> c_18(top^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_17(x1) = [1] x1 + [2]
c_18(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{top^#(mark(X)) -> c_17(top^#(proper(X)))}
and weakly orienting the rules
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, top^#(ok(X)) -> c_18(top^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{top^#(mark(X)) -> c_17(top^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [3]
c_17(x1) = [1] x1 + [0]
c_18(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ top^#(mark(X)) -> c_17(top^#(proper(X)))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, top^#(ok(X)) -> c_18(top^#(active(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ top^#(mark(X)) -> c_17(top^#(proper(X)))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, top^#(ok(X)) -> c_18(top^#(active(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ active_0(3) -> 39
, active_0(9) -> 39
, mark_0(3) -> 3
, mark_0(9) -> 3
, proper_0(3) -> 37
, proper_0(9) -> 37
, ok_0(3) -> 9
, ok_0(9) -> 9
, top^#_0(3) -> 35
, top^#_0(9) -> 35
, top^#_0(37) -> 36
, top^#_0(39) -> 38
, c_17_0(36) -> 35
, c_18_0(38) -> 35}
4) { proper^#(h(X)) -> c_11(h^#(proper(X)))
, h^#(ok(X)) -> c_16(h^#(X))
, h^#(mark(X)) -> c_6(h^#(X))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(h(X)) -> c_11(h^#(proper(X)))
, h^#(ok(X)) -> c_16(h^#(X))
, h^#(mark(X)) -> c_6(h^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(h(X)) -> c_11(h^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(h(X)) -> c_11(h^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [8]
proper^#(x1) = [1] x1 + [9]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [2]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{h^#(ok(X)) -> c_16(h^#(X))}
and weakly orienting the rules
{proper^#(h(X)) -> c_11(h^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{h^#(ok(X)) -> c_16(h^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [8]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [4]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [9]
proper^#(x1) = [1] x1 + [13]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{h^#(mark(X)) -> c_6(h^#(X))}
and weakly orienting the rules
{ h^#(ok(X)) -> c_16(h^#(X))
, proper^#(h(X)) -> c_11(h^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{h^#(mark(X)) -> c_6(h^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [8]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [8]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [4]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ h^#(mark(X)) -> c_6(h^#(X))
, h^#(ok(X)) -> c_16(h^#(X))
, proper^#(h(X)) -> c_11(h^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ h^#(mark(X)) -> c_6(h^#(X))
, h^#(ok(X)) -> c_16(h^#(X))
, proper^#(h(X)) -> c_11(h^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, h^#_0(3) -> 20
, h^#_0(9) -> 20
, c_6_0(20) -> 20
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23
, c_16_0(20) -> 20}
5) { proper^#(f(X)) -> c_7(f^#(proper(X)))
, f^#(ok(X)) -> c_12(f^#(X))
, f^#(mark(X)) -> c_5(f^#(X))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(f(X)) -> c_7(f^#(proper(X)))
, f^#(ok(X)) -> c_12(f^#(X))
, f^#(mark(X)) -> c_5(f^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{f^#(ok(X)) -> c_12(f^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(ok(X)) -> c_12(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(X)) -> c_7(f^#(proper(X)))}
and weakly orienting the rules
{f^#(ok(X)) -> c_12(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(X)) -> c_7(f^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(mark(X)) -> c_5(f^#(X))}
and weakly orienting the rules
{ proper^#(f(X)) -> c_7(f^#(proper(X)))
, f^#(ok(X)) -> c_12(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(mark(X)) -> c_5(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [8]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [8]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [9]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ f^#(mark(X)) -> c_5(f^#(X))
, proper^#(f(X)) -> c_7(f^#(proper(X)))
, f^#(ok(X)) -> c_12(f^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ f^#(mark(X)) -> c_5(f^#(X))
, proper^#(f(X)) -> c_7(f^#(proper(X)))
, f^#(ok(X)) -> c_12(f^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, f^#_0(3) -> 18
, f^#_0(9) -> 18
, c_5_0(18) -> 18
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23
, c_12_0(18) -> 18}
6) {active^#(h(X)) -> c_4(h^#(active(X)))}
The usable rules for this path are the following:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, active^#(h(X)) -> c_4(h^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(h(X)) -> c_4(h^#(active(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(h(X)) -> c_4(h^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
h^#(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))}
and weakly orienting the rules
{active^#(h(X)) -> c_4(h^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [5]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [4]
h^#(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active^#(h(X)) -> c_4(h^#(active(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active^#(h(X)) -> c_4(h^#(active(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(9) -> 11
, h^#_0(3) -> 20
, h^#_0(9) -> 20}
7) {active^#(f(X)) -> c_3(f^#(active(X)))}
The usable rules for this path are the following:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(X)) -> c_3(f^#(active(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [3]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))}
and weakly orienting the rules
{active^#(f(X)) -> c_3(f^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [3]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [5]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(9) -> 11
, f^#_0(3) -> 18
, f^#_0(9) -> 18}
8) { proper^#(g(X)) -> c_9(g^#(proper(X)))
, g^#(ok(X)) -> c_14(g^#(X))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(g(X)) -> c_9(g^#(proper(X)))
, g^#(ok(X)) -> c_14(g^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(g(X)) -> c_9(g^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(g(X)) -> c_9(g^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [12]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
g^#(x1) = [1] x1 + [8]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [9]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g^#(ok(X)) -> c_14(g^#(X))}
and weakly orienting the rules
{proper^#(g(X)) -> c_9(g^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g^#(ok(X)) -> c_14(g^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [2]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [8]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
g^#(x1) = [1] x1 + [4]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ g^#(ok(X)) -> c_14(g^#(X))
, proper^#(g(X)) -> c_9(g^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ g^#(ok(X)) -> c_14(g^#(X))
, proper^#(g(X)) -> c_9(g^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23
, g^#_0(3) -> 27
, g^#_0(9) -> 27
, c_14_0(27) -> 27}
9) { proper^#(c(X)) -> c_8(c^#(proper(X)))
, c^#(ok(X)) -> c_13(c^#(X))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(c(X)) -> c_8(c^#(proper(X)))
, c^#(ok(X)) -> c_13(c^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(c(X)) -> c_8(c^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(c(X)) -> c_8(c^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [3]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [3]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{c^#(ok(X)) -> c_13(c^#(X))}
and weakly orienting the rules
{proper^#(c(X)) -> c_8(c^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{c^#(ok(X)) -> c_13(c^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [2]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [8]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [10]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ c^#(ok(X)) -> c_13(c^#(X))
, proper^#(c(X)) -> c_8(c^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ c^#(ok(X)) -> c_13(c^#(X))
, proper^#(c(X)) -> c_8(c^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, c^#_0(3) -> 13
, c^#_0(9) -> 13
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23
, c_13_0(13) -> 13}
10)
{ proper^#(d(X)) -> c_10(d^#(proper(X)))
, d^#(ok(X)) -> c_15(d^#(X))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(d(X)) -> c_10(d^#(proper(X)))
, d^#(ok(X)) -> c_15(d^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(d(X)) -> c_10(d^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(d(X)) -> c_10(d^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [8]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [12]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{d^#(ok(X)) -> c_15(d^#(X))}
and weakly orienting the rules
{proper^#(d(X)) -> c_10(d^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{d^#(ok(X)) -> c_15(d^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [12]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [1] x1 + [8]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [12]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [3]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ d^#(ok(X)) -> c_15(d^#(X))
, proper^#(d(X)) -> c_10(d^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules:
{ d^#(ok(X)) -> c_15(d^#(X))
, proper^#(d(X)) -> c_10(d^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, d^#_0(3) -> 15
, d^#_0(9) -> 15
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23
, c_15_0(15) -> 15}
11)
{proper^#(c(X)) -> c_8(c^#(proper(X)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(c(X)) -> c_8(c^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(c(X)) -> c_8(c^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(c(X)) -> c_8(c^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(c(X)) -> c_8(c^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(c(X)) -> c_8(c^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, c^#_0(3) -> 13
, c^#_0(9) -> 13
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23}
12)
{proper^#(d(X)) -> c_10(d^#(proper(X)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(d(X)) -> c_10(d^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(d(X)) -> c_10(d^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(d(X)) -> c_10(d^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(d(X)) -> c_10(d^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(d(X)) -> c_10(d^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, d^#_0(3) -> 15
, d^#_0(9) -> 15
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23}
13)
{proper^#(f(X)) -> c_7(f^#(proper(X)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(f(X)) -> c_7(f^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(X)) -> c_7(f^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(X)) -> c_7(f^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [4]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(f(X)) -> c_7(f^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(f(X)) -> c_7(f^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, f^#_0(3) -> 18
, f^#_0(9) -> 18
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23}
14)
{proper^#(h(X)) -> c_11(h^#(proper(X)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(h(X)) -> c_11(h^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(h(X)) -> c_11(h^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(h(X)) -> c_11(h^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(h(X)) -> c_11(h^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(h(X)) -> c_11(h^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, h^#_0(3) -> 20
, h^#_0(9) -> 20
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23}
15)
{proper^#(g(X)) -> c_9(g^#(proper(X)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))
, proper^#(g(X)) -> c_9(g^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(g(X)) -> c_9(g^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(g(X)) -> c_9(g^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [4]
c(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [1] x1 + [0]
h(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
g^#(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(g(X)) -> c_9(g^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X))}
Weak Rules: {proper^#(g(X)) -> c_9(g^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, proper^#_0(3) -> 23
, proper^#_0(9) -> 23
, g^#_0(3) -> 27
, g^#_0(9) -> 27}
16)
{ active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))
, c^#(ok(X)) -> c_13(c^#(X))}
The usable rules for this path are the following:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))
, c^#(ok(X)) -> c_13(c^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [1]
mark(x1) = [1] x1 + [0]
c(x1) = [0] x1 + [0]
g(x1) = [1] x1 + [1]
d(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [0]
c^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [8]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{c^#(ok(X)) -> c_13(c^#(X))}
and weakly orienting the rules
{active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{c^#(ok(X)) -> c_13(c^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [1]
mark(x1) = [1] x1 + [0]
c(x1) = [0] x1 + [0]
g(x1) = [1] x1 + [0]
d(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [15]
c_0(x1) = [1] x1 + [0]
c^#(x1) = [1] x1 + [12]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [1]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))}
Weak Rules:
{ c^#(ok(X)) -> c_13(c^#(X))
, active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))}
Weak Rules:
{ c^#(ok(X)) -> c_13(c^#(X))
, active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(9) -> 11
, c^#_0(3) -> 13
, c^#_0(9) -> 13
, c_13_0(13) -> 13}
17)
{active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
The usable rules for this path are the following:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))
, active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [1]
mark(x1) = [1] x1 + [0]
c(x1) = [0] x1 + [0]
g(x1) = [1] x1 + [1]
d(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [8]
c_0(x1) = [1] x1 + [0]
c^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))}
Weak Rules: {active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, g(ok(X)) -> ok(g(X))}
Weak Rules: {active^#(f(f(X))) -> c_0(c^#(f(g(f(X)))))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(9) -> 3
, ok_0(3) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(9) -> 11
, c^#_0(3) -> 13
, c^#_0(9) -> 13}
18)
{ active^#(h(X)) -> c_2(c^#(d(X)))
, c^#(ok(X)) -> c_13(c^#(X))}
The usable rules for this path are the following:
{d(ok(X)) -> ok(d(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ d(ok(X)) -> ok(d(X))
, active^#(h(X)) -> c_2(c^#(d(X)))
, c^#(ok(X)) -> c_13(c^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(h(X)) -> c_2(c^#(d(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(h(X)) -> c_2(c^#(d(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
d(x1) = [1] x1 + [1]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [8]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{c^#(ok(X)) -> c_13(c^#(X))}
and weakly orienting the rules
{active^#(h(X)) -> c_2(c^#(d(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{c^#(ok(X)) -> c_13(c^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
d(x1) = [1] x1 + [1]
h(x1) = [1] x1 + [4]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [15]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [12]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [4]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [1] x1 + [1]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {d(ok(X)) -> ok(d(X))}
Weak Rules:
{ c^#(ok(X)) -> c_13(c^#(X))
, active^#(h(X)) -> c_2(c^#(d(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {d(ok(X)) -> ok(d(X))}
Weak Rules:
{ c^#(ok(X)) -> c_13(c^#(X))
, active^#(h(X)) -> c_2(c^#(d(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ ok_0(9) -> 9
, active^#_0(9) -> 11
, c^#_0(9) -> 13
, c_13_0(13) -> 13}
19)
{active^#(h(X)) -> c_2(c^#(d(X)))}
The usable rules for this path are the following:
{d(ok(X)) -> ok(d(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ d(ok(X)) -> ok(d(X))
, active^#(h(X)) -> c_2(c^#(d(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(h(X)) -> c_2(c^#(d(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(h(X)) -> c_2(c^#(d(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
d(x1) = [1] x1 + [1]
h(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {d(ok(X)) -> ok(d(X))}
Weak Rules: {active^#(h(X)) -> c_2(c^#(d(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules: {d(ok(X)) -> ok(d(X))}
Weak Rules: {active^#(h(X)) -> c_2(c^#(d(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ ok_0(2) -> 2
, active^#_0(2) -> 1
, c^#_0(2) -> 1}
20)
{ active^#(c(X)) -> c_1(d^#(X))
, d^#(ok(X)) -> c_15(d^#(X))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
d(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {d^#(ok(X)) -> c_15(d^#(X))}
Weak Rules: {active^#(c(X)) -> c_1(d^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{d^#(ok(X)) -> c_15(d^#(X))}
and weakly orienting the rules
{active^#(c(X)) -> c_1(d^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{d^#(ok(X)) -> c_15(d^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [0] x1 + [0]
d(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [1]
d^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [3]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ d^#(ok(X)) -> c_15(d^#(X))
, active^#(c(X)) -> c_1(d^#(X))}
Details:
The given problem does not contain any strict rules
21)
{active^#(c(X)) -> c_1(d^#(X))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
c(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
d(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
d^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {active^#(c(X)) -> c_1(d^#(X))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(c(X)) -> c_1(d^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(c(X)) -> c_1(d^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
c(x1) = [1] x1 + [0]
g(x1) = [0] x1 + [0]
d(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
c^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
d^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
h^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {active^#(c(X)) -> c_1(d^#(X))}
Details:
The given problem does not contain any strict rules